| 1: | le(0,y) | → true | |
| 2: | le(s(x),0) | → false | |
| 3: | le(s(x),s(y)) | → le(x,y) | |
| 4: | minus(0,y) | → 0 | |
| 5: | minus(s(x),y) | → if_minus(le(s(x),y),s(x),y) | |
| 6: | if_minus(true,s(x),y) | → 0 | |
| 7: | if_minus(false,s(x),y) | → s(minus(x,y)) | |
| 8: | gcd(0,y) | → y | |
| 9: | gcd(s(x),0) | → s(x) | |
| 10: | gcd(s(x),s(y)) | → if_gcd(le(y,x),s(x),s(y)) | |
| 11: | if_gcd(true,s(x),s(y)) | → gcd(minus(x,y),s(y)) | |
| 12: | if_gcd(false,s(x),s(y)) | → gcd(minus(y,x),s(x)) | |
| 13: | LE(s(x),s(y)) | → LE(x,y) | |
| 14: | MINUS(s(x),y) | → IF_MINUS(le(s(x),y),s(x),y) | |
| 15: | MINUS(s(x),y) | → LE(s(x),y) | |
| 16: | IF_MINUS(false,s(x),y) | → MINUS(x,y) | |
| 17: | GCD(s(x),s(y)) | → IF_GCD(le(y,x),s(x),s(y)) | |
| 18: | GCD(s(x),s(y)) | → LE(y,x) | |
| 19: | IF_GCD(true,s(x),s(y)) | → GCD(minus(x,y),s(y)) | |
| 20: | IF_GCD(true,s(x),s(y)) | → MINUS(x,y) | |
| 21: | IF_GCD(false,s(x),s(y)) | → GCD(minus(y,x),s(x)) | |
| 22: | IF_GCD(false,s(x),s(y)) | → MINUS(y,x) | |